sends1-p(es;x;A;k;B;l;tg;T;f)
== ((vartype(source(l);x) r A)
== & (e:E. (loc(e) = source(l))  (kind(e) = k)  (valtype(e) r B))
== & (e:E. (kind(e) = rcv(l,tg))  (valtype(e) r T)))
== c (e:E.
== c (loc(e) = source(l))
== c  (kind(e) = k)
== c  (L:{e':E| kind(e') = rcv(l,tg)}  List
== c  (((e':E. (e'  L)  ((kind(e') = rcv(l,tg)) c (sender(e') = e)))
== c  (& (e1, e2:E. e1 before e2  L  (e1 <loc e2))
== c  (& map(e'.val(e');L) = f((x when e),val(e))))) 

latex

---

clarification:

sends1-p(es;x;A;k;B;l;tg;T;f)
== ((es-vartype(es; source(l); x) r A)
== & (e:es-E(es).
== & ((es-loc(es; e) = source(l)  Id)  (es-kind(es; e) = k  Knd)  (es-valtype(es; e) r B))
== & (e:es-E(es). (es-kind(es; e) = rcv(l,tg)  Knd)  (es-valtype(es; e) r T)))
== c (e:es-E(es).
== c (es-loc(es; e) = source(l)  Id)
== c  (es-kind(es; e) = k  Knd)
== c  (L:{e':es-E(es)| es-kind(es; e') = rcv(l,tg)  Knd}  List
== c  (((e':es-E(es).
== c  ((((e'  L  es-E(es))
== c  ((( ((es-kind(es; e') = rcv(l,tg)  Knd) c (es-sender(es; e') = e  es-E(es))))
== c  (& (e1:es-E(es), e2:es-E(es). e1 before e2  L  es-E(es)  es-locl(es; e1; e2))
== c  (& map(e'.es-val(es; e');L) = f(es-when(es; x; e),es-val(es; e))  (T List)))) 

latex

Definitions	vartype(i;x), valtype(e), Id, loc(e), source(l), x:A. B(x), {x:A| B(x)} , P  Q, (x  l), A c B, Knd, kind(e), rcv(l,tg), sender(e), P & Q, x:A. B(x), P  Q, x before y  l, E, (e <loc e'), s = t, type List, map(f;as), x.A(x), f(a), x when e, val(e)
FDL editor aliases	sends1-p